$\forall$${\it es}$:ES, $e_{1}$:E, $e_{2}$:\{$e$:E$\mid$ loc($e$) $=$ loc($e_{1}$) $\in$ Id \}, $Q$:(\{$e$:E$\mid$ loc($e$) $=$ loc($e_{1}$) $\in$ Id \}$\rightarrow$Prop).
\\[0ex]($\forall$$e$:\{$e$:E$\mid$ loc($e$) $=$ loc($e_{1}$) $\in$ Id \}. Dec($Q$($e$)))
\\[0ex]$\Rightarrow$ ([$e_{1}$,$e_{2}$]$\sim$([$a$,$b$].$b$ = first $e$ $\geq$ $a$.$Q$($e$))+ $\Leftrightarrow$ $e_{1}$ $\leq$ $e_{2}$  \& $Q$($e_{2}$))